COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	book[e84,jmc]		Notes for modifying McCarthy and Talcott
C00005 00003	section on ekl and/or Boyer-Moore
C00006 00004	Outlines:
C00007 ENDMK
C⊗;
book[e84,jmc]		Notes for modifying McCarthy and Talcott

Notes based on version pubbed Sept. 15, 1980

page
ii
Many assertions about pure LISP programs were proved using Richard
Weyhrauch's (197x) FOL interactive theorem prover for first order logic.
In recent years Jussi Ketonen's (1984) EKL interactive theorem prover for
type theory has been used in a Stanford University course entitled
"Recursive programming and Proving" taught using this book.  The
availability of second order logic in EKL has proved advantageous.
The experience of proving facts about programs has the same advantages
as the study of any other mathematical domain.  Even if the student
never proves another theorem, his understanding of the subject is
enhanced by the experience.

The class experience with the interactive theorem provers has been
mixed.  Understanding is enhanced by using a fully formal system,
but debugging proofs is tedious with present systems, especially
when the computer being used is overloaded.

4 - It's not clear this insert should be made.
Small integers are sometimes represented by the number itself usually
with a certain constant added rather than by a pointer.  The constant
serves to give the representation a numerical value that can be
distinguished from the pointers into memory.  This scheme saves time
and memory space.

7 basic LISP programs. → basic LISP functions.

section on ekl and/or Boyer-Moore

Lisp expression whose value is itself.

Pattern matcher and proof of its correctness.

Unification algorithm and proof of its correctness.

What about Jussi's higher order unifier?

comma and backquote?
Outlines:

first the outline based on abstraction first.

abstract section
internal notation, i.e. calling lisp functions and defun.